(set-logic ALL)
(set-info :status unsat)
(declare-sort U 0)
(declare-datatypes ((D 0) (T@t 0)) (((err)) ((t (|v#t| U) (|l#t| Int)))))
(declare-sort V 0)
(declare-datatypes ((T 0) (TArray 0)) (((E) (b (B Bool)) (A (add Int)) (Vec (vec TArray))) ((Var (R V) (|l#Var| Int)))))
(declare-sort Bb 0)
(declare-datatypes ((M 0)) (((Mem (cm Bb)))))
(declare-fun mc (D) U)
(declare-fun eq (T T) Bool)
(declare-fun s (V Int) T)
(declare-fun sto (V Int T) V)
(declare-fun sel (Bb T@t Int) T)
(declare-fun c () T)
(declare-fun in () M)
(declare-fun rdv () T)
(declare-fun ivp () T)
(declare-fun ex () T)
(declare-fun cdv () T)
(assert (forall ((z T) (y T)) (! (or (= z y) (not (eq z y))) :qid Q1)))
(assert (forall ((?x0 V) (?x1 Int) (?x2 T)) (! (= ?x2 (s (sto ?x0 ?x1 ?x2) ?x1)) :qid Q2)))
(declare-fun k1 () Bool)
(declare-fun k2 () Bool)
(assert (and 
(is-Vec ex) 
(not 
  (and 
    (not (= ex E)) 
    (or 
      (not (= rdv (b false))) 
      (not (= ivp (Vec (Var (sto (R (vec cdv)) (|l#Var| (vec cdv)) c) 0)))) 
      (not (= rdv (b k1))) 
      (not (B (b k2))))))))
(assert (= k1 (not (forall ((j Int)) (! (not (eq c (s (R (vec ivp)) j))) :qid Q3)))))
(assert (= k2 (not (forall (($i_0 Int)) (! (not (B (b (eq c (s (R (vec (s (R (vec (s (R (vec (sel (cm in) (t (mc err) 1) (add (A 0))))) 0))) 0))) $i_0))))) :qid Q4)))))
(check-sat)

